1. Field of the Invention
The field of invention generally relates to formal equivalence verification tools and analyzing logic circuit models within a mathematical framework and more particularly, to an efficient method for performing sequential verification of loop-free circuits.
2. Background of the Related Art
Formal Equivalence Verification (FEV) tools are used to establish the equivalence of logic circuit models by analyzing them within a mathematical framework, thereby eliminating the need to resort to computationally intensive simulation of the circuits with very large numbers of inputs.
The logic design process can be viewed as a series of circuit model transformations that proceed from abstract Register Transfer Level (RTL) descriptions down to transistor level netlists. One of the factors upon which the correctness of the final, low level, implementation of the circuit depends upon, is the establishment of the equivalence of circuit models at differing levels of abstraction. Abstraction refers to the different levels of partition and hierarchy that may be used to model a circuit or a system under test. Two examples of different levels of abstraction are RTL and schematic levels.
FEV tools help to establish the equivalence of logic circuit models by analyzing them within a mathematical framework, without resorting to simulating a large number of input patterns. Frequently, the tools compare sequential logic circuit models that differ in terms of the number and placement of the state elements they contain. This is a direct consequence of the requirement to raise the level of abstraction for circuit descriptions and to improve the productivity of the front-end design activities. The performance of the classic formal equivalence verification algorithms drops significantly, as the number of state elements increases. As a result of this performance penalty, specialized algorithms have been developed that have increased performance for certain common categories of circuits. One such category of circuits includes pipelined loop-free circuits. The claimed embodiments of the present invention are concerned with the verification of pipelined loop-free circuits.
The related art approaches to verification of pipelined loop-free circuits has several disadvantages. The Boolean formulas that model circuit behavior are represented using binary decision diagrams (BDDs). Therefore, these approaches suffer from the well known limitations of BDDs (e.g. memory explosion). Furthermore, related art clocking schemes are rather simplistic (see R. K Ranjan, V. Singhal, F. Somenzi, and R. K Brayton, “Using Combinational Verification for Sequential Circuits” in Proceedings of Design, Automation and Test in Europe Conference, 1999).
Also, some related art approaches can only accommodate circuits with edge-triggered flip-flops (see G. P. Bischoff, K. S. Brace, S. Jain, and R. Razdan, “Formal Implementation Verification of the Bus Interface Unit for the Alpha 21264 Microprocessor” in Proceedings of IEEE International Conference on Computer Design; VLSI in Computers and Processors, 1997 and R.K Ranjan, “Design and Implementation Verification of Finite State Systems”, Ph.D. Thesis, Univ. of California, Berkeley, 1997). The exemplary embodiments of the present invention address many of these aforementioned problems.
In the claimed embodiments of the present invention, the Boolean formulas that model circuit behavior are represented using Binary Expression Diagrams. These Boolean formulas are called Timed Binary Expression Diagrams ABED). As a result of using this type of Boolean representation, the functionality of very complex circuits can be modeled without suffering from exponential memory requirements associated with the use of binary decision diagrams (BDDs). The comparison of formulas represented as Binary Expression Diagrams is performed with a satisfiability (SAT) solver.
The combinational properties on the circuit inputs as well as on internal nodes are processed, and these properties are taken into account during the construction of TBEDs.
The new algorithm for TBED computation operates in a computationally efficient manner. During a test of one exemplary embodiment of the present invention, a 120× average speedup on complex circuits with respect to older versions employing TBED construction algorithms was achieved. One reason for the increased performance is that only one traversal of the latches is needed in the verified circuits, and for each latch, two relatively simple operations (a restrict operation and a shift operation) are performed. This means that it is not necessary to compute TBEDs with non-empty event lists.